# -*- mode: Makefile; -*-
# ----------------------------------------------------------------------------
# 
# ****             pl2texi document generation SETTINGS                  *****
# 
#         These SETTINGS should be changed to suit your application
# 
# The defaults listed are suggestions and/or the ones used for local 
# installation in the CLIP group machines.
# ----------------------------------------------------------------------------
# List of all the system directories where .pl files used are
# (separated by spaces; put explicit paths, i.e., do not use any variables)
# You also need to specify all the paths of files used by those files!
# 
FILEPATHS = /home/clip/Systems/WebDB/doc
# ----------------------------------------------------------------------------
# List of all the *system* directories where .pl files used are
# (separated by spaces; put explicit paths, i.e., do not use any variables)
# You also need to specify all the paths of files used by those files!
# You can put these in FILEPATHS instead. Putting them here only
# means that the corresponding files will be assumed to be "system"
# files in the documentation.
# 
SYSTEMPATHS = \
  /home/clip/Systems/ciao-0.7/lib \
  /home/clip/Systems/ciao-0.7/library \
  /home/clip/Systems/ciao-0.7/library/persdb \
  /home/clip/Systems/ciao-0.7/contrib
# ----------------------------------------------------------------------------
# Define this to be the main file name (include a path only if it
# should appear in the documentation) 
# 
MAIN = WebDB_doc.pl
# ----------------------------------------------------------------------------
# Select pl2texi options for main file (do pl2texi -h to get a list of options)
# Leaving this blank produces most verbose manuals
# -nobugs -noauthors -noversion -nochangelog -nopatches -modes 
# -headprops -literalprops -noundefined
# 
# MAINOPTS = 
# -nopatches
MAINOPTS = -nobugs -modes -nochangelog
# ----------------------------------------------------------------------------
# List of files to be used as components. These can be .pl files
# or .src files (manually produced files in texinfo format). 
# (include a path only if it should appear in the documentation, i.e.,
# for sublibraries) 
# 
COMPONENTS = \
	dbserver_doc.pl \
	dbclients_doc.pl \
	Installation.pl 
# ----------------------------------------------------------------------------
# Select pl2texi opts for component file(s) (do pl2texi -h to get list of opts)
# Leaving this blank produces most verbose manuals
# -nobugs -noauthors -noversion -nochangelog -nopatches 
# -modes -headprops -literalprops 
# 
# COMPOPTS = 
# -nochangelog 
#COMPOPTS = -nobugs -modes -nochangelog
# ----------------------------------------------------------------------------
# Define this to be the list of documentation formats to be generated by 
# default when typing gmake
# 
# DOCFORMATS = @echo Please do "gmake <target>"
# DOCFORMATS = dvi ps html htmlindex info infoindex manl 
DOCFORMATS = dvi ps html htmlindex info infoindex 
# ----------------------------------------------------------------------------
# Define this to be the list (separated by spaces) of indices to be 
# generated ('all' generates all the supported indices)
# Note: too many indices may exceed the capacity of texinfo!
# 
# INDICES=concept lib apl pred prop type decl op modedef file usage
# INDICES=all
INDICES=concept pred type usage
# ----------------------------------------------------------------------------
# Only need to change these if you will be installing the docs somewhere else
# ----------------------------------------------------------------------------
# Define this to be the dir in which you want the document(s) installed. 
# 
# DOCDIR= /usr/local/doc
DOCDIR=/home/clip/public_html/Local/pl2texi_docs
# ----------------------------------------------------------------------------
# Uncomment this for .dvi and .ps files to be compressed on installation
# If uncommented, set it to path for gzip
# 
# COMPRESSDVIPS = gzip
# ----------------------------------------------------------------------------
# Define this to be the permissions for automatically generated data files
# 
DATAMODE = 664
# ----------------------------------------------------------------------------
# Define this to be the perms for automatically generated dirs and exec files
# 
EXECMODE = 775
# ----------------------------------------------------------------------------
# The settings below are important only for generating html and info *indices*
# ----------------------------------------------------------------------------
# Define this to be files containing header and tail for the html index. 
# Pointers to the files generated by pl2texi are placed in a document that 
# starts with HTMLINDEXHEADFILE and finishes with HTMLINDEXTAILFILE
# 
# HTMLINDEXHEADFILE = $(LIBDIR)/Head_generic.html
HTMLINDEXHEADFILE = $(LIBDIR)/Head_clip.html
# HTMLINDEXTAILFILE = $(LIBDIR)/Tail_generic.html
HTMLINDEXTAILFILE = $(LIBDIR)/Tail_clip.html
# ----------------------------------------------------------------------------
# Define this to be files containing header and tail for the info "dir" index. 
# dir entries generated by pl2texi are placed in a "dir" file that 
# starts with INFODIRHEADFILE and finishes with INFODIRTAILFILE
#
# INFODIRHEADFILE = $(LIBDIR)/Head_generic.info
INFODIRHEADFILE = $(LIBDIR)/Head_clip.info
# INFODIRTAILFILE = $(LIBDIR)/Tail_generic.info
INFODIRTAILFILE = $(LIBDIR)/Tail_clip.info
# ----------------------------------------------------------------------------
# end of SETTINGS
# ----------------------------------------------------------------------------
# PL2TEXI=/home/clip/Systems/pl2texi/src/pl2texi
PL2TEXI=/home/clip/bin/pl2texi-1.6
LIBDIR=/home/clip/lib/pl2texi-1.6
